a:. atomic(a)  {(a ~ 1) & (b:. b | a  (b ~ 1)  (b ~ a))} 

latex

Definitions	atomic(a), {T}, P  Q, P  Q, False, reducible(a), P & Q, A, P  Q, b | a, P  Q, Prop, a ~ b, x:A. B(x), t  T, Stable{P}, Dec(P), x:A. B(x), a  b, , T, True
Lemmas	assoced inversion, int entire, mul cancel in assoced, assoced elim, or functionality wrt iff, any divs zero, true wf, squash wf, assoced weakening, multiply functionality wrt assoced, assoced functionality wrt assoced, not functionality wrt iff, int nzero wf, nequal wf, zero ann b, not over or, decidable assoced, decidable or, stable from decidable, assoced wf, divides wf, reducible wf, not wf